Nuprl Lemma : concat_wf
0,22
postcript
pdf
T
:Type,
ll
:(
T
List) List. concat(
ll
)
T
List
latex
Definitions
concat(
ll
)
,
reduce(
f
;
k
;
as
)
,
as
@
bs
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
append
wf
,
reduce
wf
origin
T:Type, ll:(T List) List. concat(ll) 
T List T:Type, ll:(T List) List. concat(ll) T List x:A. B(x) T